ABS: if a=1 b then x else y

ABS: '$x'1

ABS: '$x'2

STM: atom1 sq

STM: atom2 sq

ABS: eq_atom$n(x;y)

STM: eq atom wf1

STM: eq atom wf2

STM: decidable atom equal 1

STM: decidable atom equal 2

STM: assert of eq atom1

STM: assert of eq atom2

STM: neg assert of eq atom1

STM: atom-test1

ABS: x:T||a

DIR: atoms-paper

STM: free-from-atom wf1

STM: free-from-atom wf2

STM: free-from-atom-outl

STM: free-from-atom-outr

STM: free-from-atom-nat

STM: free-from-atom-l member

STM: free-from-atom-subtype

STM: free-from-atom-int

ABS: |x|

STM: abs-val wf